/* 
 * $Id: DotVisBackend.java 1259 2007-01-09 14:23:47Z tcoupaye $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright 2004
 *    Distributed Systems Research Group
 *    Department of Software Engineering
 *    Faculty of Mathematics and Physics
 *    Charles University, Prague
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Jan Kofron <kofron@nenya.ms.mff.cuni.cz>
 */

package org.objectweb.fractal.bpc.checker.backend;


import java.util.TreeSet;
import java.io.FileOutputStream;
import java.io.IOException;
import java.io.FileNotFoundException;

import org.objectweb.fractal.bpc.checker.CheckingResult;
import org.objectweb.fractal.bpc.checker.DFSR.*;
import org.objectweb.fractal.bpc.checker.node.*;
import org.objectweb.fractal.bpc.checker.optimizer.*;
import org.objectweb.fractal.bpc.checker.parser.Debug;
import org.objectweb.fractal.bpc.checker.state.Signature;
import org.objectweb.fractal.bpc.checker.visualization.*;

/**
 * This class is intended to visualize the parse trees and resulting automaton of protocol being checked.
 */
public class DotVisBackend implements IBackend {

    public DotVisBackend(ActionRepository repository) {
        this.repository = repository;
    }

    /**
     * @see org.objectweb.fractal.bpc.checker.backend.IBackend#perform(org.objectweb.fractal.bpc.checker.node.TreeNode[], java.lang.String[], java.lang.String[])
     */
    public CheckingResult perform(TreeNode[] nodes, String[] synchroops, String[] unboundops) {
        //basic checking of parameters
        //basic checking of parameters
        if (nodes.length < 2) {
            return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Visualization backend: wrong number of items within the first array parameter (at least two required.\n");
        }

        if (synchroops.length != nodes.length - 1) {
            return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Visualization backend: wrong number of items within the second array parameter (1 lower than the number of components required).\n");
        }

        DotVisualizer dotviz = new DotVisualizer(repository);

        // parse tree visualization
        for (int i = 0; i < nodes.length; ++i) {

            dotviz.visualize(nodes[i], "pt_" + i + ".dt");

        }

        /*
        try {
            for (int i = 0; i < nodes.length; ++i) {

                Signature.setSize(nodes[i].getLeafCount());

                FileOutputStream outputfile = new FileOutputStream("a_" + i + ".dt");

                outputfile.write("digraph G {\n  size = \"7,11\";\n".getBytes());
                new DFSRTraverser(nodes[i], repository).run(new DFSRDotVis(outputfile, nodes[i], repository));
                outputfile.write(("\n}").getBytes());

                outputfile.close();

                Debug.println("Automaton for protocol written to a_" + i + ".dt");
            }
        } catch (IOException e) {
            return "Error while writing to the file a_?.dt";
        } catch (InvalidParameterException e) {
            return "Error while checking (Invalid parameter exception): " + e.getMessage();
        } catch (ItemAlreadyPresentException e) {
            return "Error while checking (ItemAlreadyPresentException): " + e.getMessage();
        } catch (ItemNotPresentException e) {
            return "Error while checking (ItemNotPresentException): " + e.getMessage();
        } catch (CheckingException e) {
            return "End of checking while vizualizating, need a fix! - " + e.getMessage();
        }
        */
        nodes[0] = ConsentBackend.invertProtocol(nodes[0], repository);

        TreeNode result = new DeterministicNode(nodes[nodes.length - 1]);

        TreeSet unbound = new TreeSet();
        for (int y = 0; y < unboundops.length; ++y) {
            unbound.add(new Integer(repository.getItemIndex(unboundops[y])));
        }

        for (int j = nodes.length - 2; j > 0; --j) {
            String[] sprov;
            TreeSet prov = new TreeSet();
            sprov = synchroops[j].equals("") ? new String[0] : synchroops[j].split(",");

            for (int i = 0; i < sprov.length; ++i) {
                int index;
                try {
                    index = repository.getItemIndex(sprov[i]);
                }
                catch (NullPointerException e) {
                      continue;
                    //return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Invalid provisions '" + sprov[i] + "' - not occuring within the protocols.");
                } 

                prov.add(new Integer(index));
            }

            // create the consent node joining the two protocols
            result = new ConsentNode(new DeterministicNode(nodes[j]), result, prov, unbound, repository, false);
                
        }

        String[] sprov;
        TreeSet prov = new TreeSet();
        sprov = synchroops[0].equals("") ? new String[0] : synchroops[0].split(",");

        for (int i = 0; i < sprov.length; ++i) {
            int index;
            try {
                index = repository.getItemIndex(sprov[i]);
            }
            catch (NullPointerException e) {
                //return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Invalid provisions '" + sprov[i] + "' - not occuring within the protocols.");
                continue;
            } 
            prov.add(new Integer(index));
        }

        ConsentNode top = new ConsentNode(new DeterministicNode(nodes[0]), result, prov, unbound, repository, false);

        Debug.println("State space estimate: " + top.getWeight());

        // perform the forward cutting and explicit optimizations
        Debug.print("Optimizing the parse tree for the composition test......");
        try {
            if (Options.forwardcutting)
                top = (ConsentNode) top.forwardCut(repository.getAllUsedEventIndices());
            
            if (top != null)
                Signature.setSize(top.getLeafCount());

            if ((Options.explicit) && (top != null))
                top = (ConsentNode) new OptExplicit(top, Options.explicitsize).perform();
        } catch (InvalidParameterException e) {
            return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Error while performing optimization. Bailing out....");
        }

        Debug.println("done.");
        /**/

        if (top != null) {
            DFSRTraverser dfsr1 = new DFSRTraverser(top, repository);

            try {
                FileOutputStream outputfile = new FileOutputStream("a_main.dt");

                outputfile.write("digraph G {\n  size = \"7,11\";\n".getBytes());
                dfsr1.run(new DFSRDotVis(outputfile, top, repository));
                outputfile.write(("\n}").getBytes());

                outputfile.close();
            } catch (CheckingException e) {
                return new CheckingResult(CheckingResult.ERR_OTHERERROR, "End of checking while vizualizating, need a fix! - " + e.getMessage());
            } catch (InvalidParameterException e) {
                return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Error while checking (Invalid parameter exception): " + e.getMessage());
            } catch (ItemAlreadyPresentException e) {
                return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Error while checking (ItemAlreadyPresentException): " + e.getMessage());
            } catch (ItemNotPresentException e) {
                return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Error while checking (ItemNotPresentException): " + e.getMessage());
            } catch (FileNotFoundException e) {
                return new CheckingResult(CheckingResult.ERR_OTHERERROR, "Couldn't open file automaton1.dt");
            } catch (IOException e) {
                return new CheckingResult(CheckingResult.ERR_OTHERERROR, "IOException while writing to the file a_main.dt");
            }
        }

        return null;
    }

    //----------------------------------------------------------------------------------
    /**
     * Action repository
     */
    private ActionRepository repository;

    /** @link dependency */
    /* # org.objectweb.fractal.bpc.checker.parser.Builder lnkBuilder; */

    /** @link dependency */
    /* # DFSRTraverser lnkDFSRTraverser; */
}
